package karpiel.boguchwal.wojciech.przemek

import karpiel.boguchwal.wojciech.przemek.Ast._

object StdLib {

  object BBool {
    val bBool = SumType(UnitType, UnitType)
    val bFalse = SumInl(UnitValue, UnitType)
    val bTrue = SumInr(UnitType, UnitValue)

    // Type -> ifFalse -> ifTrue -> bool -> Type
    val bElim = //todo completely not checked this
      PiValue(Universe(0),
        PiValue(Bruijn(0),
          PiValue(Bruijn(1),
            PiValue(bBool, PiElim(SumElim(PiValue(UnitType, Bruijn(3)), PiValue(UnitType, Bruijn(2))), Bruijn(0))))))
  }

  object Nat {
    val natType = WType(PiValue(BoolType, PiElim(BoolElim(UnitType, EmptyType), Bruijn(0))))
    val zero = WSup(natType, BoolFalse, PiValue(EmptyType, PiElim(EmptyElim(natType), Bruijn(0))))
    val one = WSup(natType, BoolTrue, PiValue(UnitType, zero))
    val succ = PiValue(natType, WSup(natType, BoolTrue, PiValue(UnitType, Bruijn(1))))

    val natToNat = PiValue(natType, natType)
    val double = WElim(natToNat,
      PiValue(BoolType, // a : Bool
        PiElim(
          BoolRec(
            PiValue(BoolType,
              PiType(
                PiType(PiElim(natType.arityFn, Bruijn(0)), natType) //f: Ba -> nat
                , PiType(
                  PiType(PiElim(natType.arityFn, Bruijn(1)), natType), //g: ba -> nat
                  natType)
              )
            )
            ,
            PiValue(PiType(UnitType, natType),
              PiValue(PiType(UnitType, natType),
                PiElim(succ, PiElim(succ, PiElim(Bruijn(0), UnitValue))))
            ), //iftrue
            PiValue(PiType(EmptyType, natType),
              PiValue(PiType(EmptyType, natType),
                zero
              )) //iffalse
          )

          , Bruijn(0) //a
        )
      ))
  }

}


/*
To pod spodem to wyjaśnienie dla mnie samego dlaczego dla zdefniowania
mnożenia przez 2 jako W-Typu jest potrzebne Bool_rec
a nie wystarczy Bool_ind
i to jeszcze Bool_rec użyte w nieoczywisty sposób (tzn inaczej niż naiwne podejście- umieszczenie Bool_rec
jak najgłębiej podczas gdy powinno być jak najwyżej żeby polimorfizm typu objął jak najwięcej drzewa)

Require Import HoTT.

(* defninicja liczb naturalnych jako W-typu *)
Definition NatConstrCount := Bool.
Definition NatConstrArity := Bool_ind (fun _ => Type) Unit Empty.
Definition NatW: Type := W NatConstrCount NatConstrArity.

Definition NatSup := sup NatConstrCount NatConstrArity.
Definition ZW: NatW :=  NatSup false (Empty_rect (fun _ => NatW)).
Definition SuccW (n: NatW): NatW
  := NatSup true (fun _: (NatConstrArity true) => n).

Definition OneW := SuccW ZW.
Check OneW.
Check W_ind.
Check W_rec.
Check Bool_ind.
Check Bool_rec.
Definition Double: NatW -> NatW
  := W_rec NatConstrCount NatConstrArity (fun _ => NatW)
           (fun l: Bool =>
           (Bool_ind
              (fun lq => (( (NatConstrArity lq)-> NatW) -> ((NatConstrArity lq) -> NatW) -> NatW))
               (fun u: Unit -> NatW => (fun q: Unit -> NatW  =>(SuccW (SuccW (q tt)))))
               (fun  z t => ZW )
               l
               ))
.

Definition NIEDZIAŁAJĄCEDouble: NatW -> NatW
  := W_rec NatConstrCount NatConstrArity (fun _ => NatW)
           (fun l: Bool =>
           (Bool_rec (*!!!!!!!!!!!!! nie ma już fun lq!*)
              ( (( (NatConstrArity l)-> NatW) -> ((NatConstrArity l) -> NatW) -> NatW))
               (fun u: Unit -> NatW => (fun q: Unit -> NatW  =>(SuccW (SuccW (q tt)))))
               (fun  z t => ZW )
               l
               ))
           .

Błąd kompilacji rego ostatniego:
Error: Found type "Unit -> NatW" where
"NatConstrArity l -> NatW" was expected.

Dokładnie to samo co u mnie:
java.lang.IllegalStateException: PiElim(BoolElim(UnitType,EmptyType),Bruijn(2)) !== UnitType


  */